<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Lean papers</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  

  <div class="row mt-3">
    <div class="col">
      <h1>Papers</h1>
      
      <h2 class="mt-3">Papers about Lean</h2>
      <ul>
        
        <li>Daniel Selsam, Simon Hudon, Leonardo de Moura, 
          <a href="https://arxiv.org/abs/2003.01685">Sealing Pointer-Based Optimizations Behind Pure Functions</a>
          
          2020
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean4</span></small>
          
        </li>
        
        <li>Daniel Selsam, Sebastian Ullrich, Leonardo de Moura, 
          <a href="https://arxiv.org/abs/2001.04301">Tabled Typeclass Resolution</a>
          
          2020
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean4</span></small>
          
        </li>
        
        <li>Sebastian Ullrich, Leonardo de Moura, 
          <a href="https://arxiv.org/abs/2001.10490">Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages</a>
          
          2020
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean4</span></small>
          
        </li>
        
        <li>Mario Carneiro, 
          <a href="https://github.com/digama0/lean-type-theory/releases">The Type Theory of Lean</a>
          
          2019
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Marc Huisinga, 
          <a href="https://pp.ipd.kit.edu/uploads/publikationen/huisinga19bachelorarbeit.pdf">Formally Verified Insertion of Reference Counting Instructions</a>
          
          2019
           (<a href="https://github.com/mhuisi/rc-correctness">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean4</span></small>
          
        </li>
        
        <li>Sebastian Ullrich, Leonardo de Moura, 
          <a href="http://arxiv.org/abs/1908.05647">Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming</a>
          
          2019
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean4</span></small>
          
        </li>
        
        <li>Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura, 
          <a href="https://doi.org/10.1145/3110278">A metaprogramming framework for formal verification</a>
          PACMPL,
          2017
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Daniel Selsam, Leonardo de Moura, 
          <a href="https://doi.org/10.1007/978-3-319-40229-1_8">Congruence Closure in Intensional Type Theory</a>
          Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings,
          2016
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean2</span></small>
          
        </li>
        
        <li>Leonardo de Moura, Jeremy Avigad, Soonho Kong, Cody Roux, 
          <a href="https://arxiv.org/pdf/1505.04324.pdf">Elaboration in Dependent Type Theory</a>
          
          2015
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean2</span></small>
          
        </li>
        
        <li>Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer, 
          <a href="https://doi.org/10.1007/978-3-319-21401-6_26">The Lean Theorem Prover (System Description)</a>
          Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings,
          2015
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean2</span></small>
          
        </li>
         
      </ul>
      
      <h2 class="mt-3">Papers about mathlib</h2>
      <ul>
        
        <li>Anne Baanen, 
          <a href="https://lean-forward.github.io/ring_exp/paper.pdf">A Lean tactic for normalising ring expressions with exponents</a>
          
          2020
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Robert Lewis, Paul-Nicolas Madelaine, 
          <a href="https://arxiv.org/abs/2001.10594">Simplifying Casts and Coercions</a>
          Practical Aspects of Automated Reasoning, PAAR 2020,
          2020
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li> The mathlib community, 
          <a href="https://doi.org/10.1145/3372885.3373824">The Lean mathematical library</a>
          Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020,
          2020
           (<a href="https://leanprover-community.github.io/">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Floris van Doorn, Gabriel Ebner, Robert Lewis, 
          <a href="https://arxiv.org/abs/2004.03673">Maintaining a Library of Formal Mathematics</a>
          Intelligent Computer Mathematics, CICM 2020,
          2020
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Paul-Nicolas Madelaine, 
          <a href="https://lean-forward.github.io/norm_cast/norm_cast.pdf">Arithmetic and Casting in Lean</a>
          
          2019
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Robert Lewis, 
          <a href="https://doi.org/10.4204/EPTCS.262.4">An Extensible Ad Hoc Interface between Lean and Mathematica</a>
          Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 September 2017,
          2017
           (<a href="https://robertylewis.com/leanmm/">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
         
      </ul>
      
      <h2 class="mt-3">Formalization papers using Lean</h2>
      <ul>
        
        <li>Kevin Buzzard, Johan Commelin, Patrick Massot, 
          <a href="https://doi.org/10.1145/3372885.3373830">Formalising perfectoid spaces</a>
          Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020,
          2020
           (<a href="https://leanprover-community.github.io/lean-perfectoid-spaces/">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Jesse Han, Floris van Doorn, 
          <a href="https://doi.org/10.1145/3372885.3373826">A formal proof of the independence of the continuum hypothesis</a>
          Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020,
          2020
           (<a href="https://flypitch.github.io/">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Mario Carneiro, 
          <a href="https://doi.org/10.4230/LIPIcs.ITP.2019.12">Formalizing Computability Theory via Partial Recursive Functions</a>
          10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA,
          2019
           (<a href="https://github.com/leanprover-community/mathlib/tree/master/src/computability">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Sander Dahmen, Johannes Hölzl, Robert Lewis, 
          <a href="https://doi.org/10.4230/LIPIcs.ITP.2019.15">Formalizing the Solution to the Cap Set Problem</a>
          10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA,
          2019
           (<a href="https://github.com/lean-forward/cap_set_problem">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Ramon Mir, 
          <a href="https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf">Schemes in Lean</a>
          
          2019
           (<a href="https://github.com/ramonfmir/lean-scheme">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Jesse Han, Floris van Doorn, 
          <a href="https://doi.org/10.4230/LIPIcs.ITP.2019.19">A Formalization of Forcing and the Unprovability of the Continuum Hypothesis</a>
          10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA,
          2019
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Robert Lewis, 
          <a href="https://doi.org/10.1145/3293880.3294089">A formal proof of Hensel's lemma over the p-adic integers</a>
          Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019,
          2019
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Neil Strickland, Nicola Bellumat, 
          <a href="https://arxiv.org/abs/1907.07801">Iterated chromatic localisation</a>
          
          2019
           (<a href="https://github.com/NeilStrickland/itloc">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean3</span></small>
          
        </li>
        
        <li>Floris van Doorn, 
          <a href="https://doi.org/10.1145/2854065.2854076">Constructing the propositional truncation using non-recursive HITs</a>
          Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016,
          2016
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean2</span></small>
          
        </li>
        
        <li>Sebastian Ullrich, 
          <a href="https://github.com/Kha/masters-thesis/blob/master/main.pdf">Simple Verification of Rust Programs via Functional Purification</a>
          
          2016
           (<a href="https://github.com/Kha/electrolysis">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean2</span></small>
          
        </li>
        
        <li>Jakob von Raumer, 
          <a href="https://doi.org/10.1007/978-3-319-42432-3_4">Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover</a>
          Mathematical Software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings,
          2016
          
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean2</span></small>
          
        </li>
        
        <li>Jakob von Raumer, 
          <a href="http://www.contrib.andrew.cmu.edu/~avigad/Students/von_raumer_thesis.pdf">Formalization of Non-Abelian Topology for Homotopy Type Theory</a>
          
          2015
           (<a href="https://github.com/javra/msc-thesis">website</a>)
          
          <small class="align-middle"><span class="badge badge-secondary align-middle">lean2</span></small>
          
        </li>
         
      </ul>
       

      <p class="mt-4">You can find all those papers and more in <a href="lean.bib">lean.bib</a>.</p>
    </div>
  </div>


  </div>
</div>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>